/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.subscope;

import java.util.Collections;
import java.util.Iterator;
import java.util.Set;
import java.util.TreeSet;

import alloy.ast.BinaryExpr;
import alloy.ast.LeafId;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.Mapper;
import alloy.util.Msg;
import alloy.util.Predicate;
import alloy.util.Util;

/**
 * An annotation for an expression giving information about its set memberships, beyond
 * what can be inferred from its relation type.  In particular, three pieces of information
 * are available:
 * <ul>
 * <li><b>Restricted-to set</b>: a set of {@link RelAnnotations} with the meaning that the tuples
 * of the expression with this info must be contained in the union of the sets of tuples associated
 * with the annotations.
 * <li><b>Excluded set</b>: a set of {@link RelAnnotations}, such that no tuple associated with any of
 * the excluded annotations can be in the expression with this info.
 * <li><b>Identity</b>: a {@link RelAnnotation} that the expression with this info is equal to, or
 * <code>null</code> if no such annotation can be determined.  
 */
public class ExprRelationInfo implements Cloneable {

    public Set /* of RelAnnotation */ restrictedTo;

    public Set /* of RelAnnotation */ excluded;

    public Set /* of RelAnnotation */ identity;

    private RelationType _type;

    private ScopedSigsInfo _scopedSigsInfo;

    public ExprRelationInfo(Set restrictedTo_, Set excluded_, Set identity_,
                            RelationType type_, ScopedSigsInfo scopedSigsInfo_) {
        this.restrictedTo = restrictedTo_;
        this.excluded = excluded_;
        this.identity = identity_;
        this._type = type_;
        this._scopedSigsInfo = scopedSigsInfo_;
    }

    public static ExprRelationInfo empty(RelationType type_, ScopedSigsInfo scopedSigsInfo_) {
        return new ExprRelationInfo(Collections.EMPTY_SET,
                                    Collections.singleton(RelAnnotation.fromType(type_, scopedSigsInfo_)),
                                    Collections.EMPTY_SET, type_, scopedSigsInfo_);
    }
    
    public ExprRelationInfo join(ExprRelationInfo other_, BinaryExpr expr_) {
        // construct dummy ExprRelationInfo objects for the join
        // column, to check if join can be non-empty
        RelationType resultType = null;
        try {
            resultType = _type.join(other_._type);
        } catch (Exception e_) {
            Dbg.fatal("shouldn't happen");
        }
        ExprRelationInfo leftDummy = _onlyColumn(_type.numBasicTypes() - 1);
        ExprRelationInfo rightDummy = other_._onlyColumn(0);
        if (!leftDummy._canIntersect(rightDummy)) {
            Dbg.warn(new Msg("result of join will always be empty set",
                                 expr_));
            return ExprRelationInfo.empty(resultType, _scopedSigsInfo);
        }
        Set /* of RelAnnotation */ joinRestricted = new TreeSet();
        for (Iterator myRestIter = restrictedTo.iterator(); myRestIter.hasNext(); ) {
            RelAnnotation myCurRest = (RelAnnotation)myRestIter.next();
            for (Iterator otherRestIter = other_.restrictedTo.iterator();
                 otherRestIter.hasNext(); ) {
                RelAnnotation otherCurRest = (RelAnnotation)otherRestIter.next();
                RelAnnotation curJoin = myCurRest.join(otherCurRest);
                if (curJoin != null) joinRestricted.add(curJoin);
            }
        }
        // for excluded, do the following:
        // X(e) = Xj(e_l) -> t_rj + t_lj -> Xj(e_r), where Xj represents the
        // excluded set with all the joined columns removed, t_lj is the type of
        // e_l without the join column, and t_rj is the type of e_r without the
        // join column.  Each element in the Xj sets is considered iff the other sides
        // join column is restricted to be inside the join column of that element.  
        // Note that if e_l or e_r has arity one, it cannot contribute
        // anything to the excluded set 
        Set /* of RelAnnotation */ joinExcluded = new TreeSet();
        RelationType joinColumnType = new RelationType(_type.getBasicTypeAt(_type.numBasicTypes() - 1));
        RelationType leftJoinedType = null;
        RelationType rightJoinedType = null;
        try {
            if (_type.numBasicTypes() > 1) {
                leftJoinedType = RelationType.join(_type, joinColumnType);
                _addIfColRestricted(other_.excluded, restrictedTo, _type.numBasicTypes() - 1, 0, leftJoinedType, joinExcluded);
            }
            if (other_._type.numBasicTypes() > 1) {
                rightJoinedType = RelationType.join(joinColumnType, other_._type);
                _addIfColRestricted(excluded, other_.restrictedTo, 0, _type.numBasicTypes() - 1, rightJoinedType, joinExcluded);
            }
        } catch (Exception e_) {
            Dbg.fatal("shouldn't happen");
        }
        // for now, just handle the case where identity sets each have one annotation
        // may be able to do something more clever for larger sets, but i'm not sure what
        Set joinIdentity = null;
        if (identity.size() == 1 && other_.identity.size() == 1) {
            RelAnnotation myIden = (RelAnnotation)identity.iterator().next();
            RelAnnotation otherIden = (RelAnnotation)other_.identity.iterator().next();
            // need to check that join column of myIden is identical to join column
            // of otherIden
            if (myIden.relIdAt(_type.numBasicTypes() - 1).equals(otherIden.relIdAt(0))) {
                joinIdentity = Collections.singleton(myIden.join(otherIden));
            } else {
                joinIdentity = Collections.EMPTY_SET;
            }
        } else {
            joinIdentity = Collections.EMPTY_SET;
        }
        return new ExprRelationInfo(joinRestricted, joinExcluded,
                                    joinIdentity, resultType, _scopedSigsInfo);
    }

    private void _addIfColRestricted(Set toBeAdded_, Set other_, final int checkColumn_,
                                     int removeColumn_, RelationType joinedType_, Set result_) {
        for (Iterator addedIter = toBeAdded_.iterator(); addedIter.hasNext(); ) {
            final RelAnnotation curAdd = (RelAnnotation)addedIter.next();
            final LeafId removeId = curAdd.relIdAt(removeColumn_);
            boolean canAdd = Util.forAll(other_, new Predicate() {
                    public boolean test(Object obj_) {
                        return _scopedSigsInfo.extendsOrEquals(((RelAnnotation)obj_).relIdAt(checkColumn_),
                                                               removeId);
                    }});
            if (canAdd) {
                RelAnnotation toAdd = curAdd.withoutColumn(removeColumn_);
                if (joinedType_ != null)
                    toAdd = toAdd.product(RelAnnotation.fromType(joinedType_, _scopedSigsInfo));
                result_.add(toAdd);
            }
        }
    }

    /**
     * @param expr_ the union expression which the resulting ExprRelationInfo
     * is annotating, or <code>null</code> if the result is not for a union
     * expr
     */
    public ExprRelationInfo union(ExprRelationInfo other_, BinaryExpr expr_) {
        // first, check that neither set must be contained in the
        // other
        if (_in(identity, other_.identity)) {
            if (expr_ != null) {
                Dbg.warn(new Msg(expr_.getLeft().nodeString() + " contained in " + expr_.getRight().nodeString(),
                                     expr_));
            }
            return other_;
        } else if (_in(other_.identity, identity)) {
            if (expr_ != null) {
                Dbg.warn(new Msg(expr_.getRight().nodeString() + " contained in " + expr_.getLeft().nodeString(),
                                     expr_));
            }
            return this;
        }
        Set /* of RelAnnotation */ unionRestricted = new TreeSet();
        _addIfLargest(restrictedTo, other_.restrictedTo, unionRestricted);
        _addIfLargest(other_.restrictedTo, restrictedTo, unionRestricted);
        Set /* of RelAnnotation */ unionExcluded = new TreeSet();
        _addIfSmallestAndCommon(excluded, other_.excluded, unionExcluded);
        _addIfSmallestAndCommon(other_.excluded, excluded, unionExcluded);
        Set /* of RelAnnotation */ unionIdentity = new TreeSet();
        unionIdentity.addAll(identity);
        unionIdentity.addAll(other_.identity);
        return new ExprRelationInfo(unionRestricted, unionExcluded, unionIdentity, _type, _scopedSigsInfo); 
    }

    private boolean _in(Set subset_, final Set superset_) {
        if (subset_.isEmpty() || superset_.isEmpty()) return false;
        return Util.forAll(subset_, new Predicate() {
                public boolean test(Object obj_) {
                    final RelAnnotation annot = (RelAnnotation)obj_;
                    return Util.forSome(superset_, new Predicate() {
                            public boolean test(Object obj2_) {
                                return annot.in((RelAnnotation)obj2_);
                            }});
                }});
    }
    public ExprRelationInfo diff(ExprRelationInfo other_, BinaryExpr expr_) {
        // check that the sets can intersect
        if (!_canIntersect(other_)) {
            Dbg.warn(new Msg(expr_.getLeft().nodeString() + " cannot intersect " + expr_.getRight().nodeString(),
                                 expr_));
            return this;
        }
        // also check left not contained in right
        if (_in(identity, other_.identity)) {
            Dbg.warn(new Msg(expr_.getLeft().nodeString() + " contained in " + expr_.getRight().nodeString(),
                                 expr_));
            return ExprRelationInfo.empty(_type, _scopedSigsInfo);
        }
        Set /* of RelAnnotation */ diffExcluded = new TreeSet();
        // can only restrict excluded further if we know what other_ is
        // identical to
        _addIfLargest(excluded, other_.identity, diffExcluded);
        _addIfLargest(other_.identity, excluded, diffExcluded);
        return new ExprRelationInfo(restrictedTo,
                                    diffExcluded,
                                    Collections.EMPTY_SET, _type, _scopedSigsInfo);
    }
        
    public ExprRelationInfo intersect(ExprRelationInfo other_, BinaryExpr expr_) {
        // check that the sets can intersect
        if (!_canIntersect(other_)) {
            Dbg.warn(new Msg(expr_.getLeft().nodeString() + " cannot intersect " + expr_.getRight().nodeString(),
                                 expr_));
            return ExprRelationInfo.empty(_type, _scopedSigsInfo);
        }
        // also check left not contained in right and vice-versa
        if (_in(identity, other_.identity)) {
            if (expr_ != null) {
                Dbg.warn(new Msg(expr_.getLeft().nodeString() + " contained in " + expr_.getRight().nodeString(),
                                     expr_));
            }
            return this;
        } else if (_in(other_.identity,identity)) {
            if (expr_ != null) {
                Dbg.warn(new Msg(expr_.getRight().nodeString() + " contained in " + expr_.getLeft().nodeString(),
                                     expr_));
            }
            return other_;
        }
        Set /* of RelAnnotation */ intersectRestricted = new TreeSet();
        _addIfSmallest(restrictedTo, other_.restrictedTo, intersectRestricted);
        _addIfSmallest(other_.restrictedTo, restrictedTo, intersectRestricted);
        Set /* of RelAnnotation */ intersectExcluded = new TreeSet();
        _addIfLargest(excluded, other_.excluded, intersectExcluded);
        _addIfLargest(other_.excluded, excluded, intersectExcluded);
        return new ExprRelationInfo(intersectRestricted,
                                    intersectExcluded,
                                    Collections.EMPTY_SET, _type, _scopedSigsInfo);
    }
        
    public ExprRelationInfo product(ExprRelationInfo other_) {
        Set /* of RelAnnotation */ prodRestricted = new TreeSet();
        // take product of all pairs of RelAnnotations, one from
        // this, one from other_
        for (Iterator myRestIter = restrictedTo.iterator();
             myRestIter.hasNext(); ) {
            RelAnnotation myCurRest = (RelAnnotation)myRestIter.next();
            for (Iterator otherRestIter = other_.restrictedTo.iterator();
                 otherRestIter.hasNext(); ) {
                RelAnnotation otherCurRest = (RelAnnotation)otherRestIter.next();
                prodRestricted.add(myCurRest.product(otherCurRest));
            }
        }
        Set /* of RelAnnotation */ prodExcluded = new TreeSet();
        RelAnnotation leftTypeAnnotation = RelAnnotation.fromType(_type, _scopedSigsInfo);
        RelAnnotation rightTypeAnnotation = RelAnnotation.fromType(other_._type, _scopedSigsInfo);
        for (Iterator myExIter = excluded.iterator(); myExIter.hasNext(); ) {
            prodExcluded.add(((RelAnnotation)myExIter.next()).product(rightTypeAnnotation));
        }
        for (Iterator otherExIter = other_.excluded.iterator(); otherExIter.hasNext(); ) {
            prodExcluded.add(((RelAnnotation)otherExIter.next()).product(leftTypeAnnotation));
        }
        Set /* of RelAnnotation */ prodIdentity = new TreeSet();
        for (Iterator myIdenIter = identity.iterator(); myIdenIter.hasNext(); ) {
            RelAnnotation myIden = (RelAnnotation)myIdenIter.next();
            for (Iterator otherIdenIter = other_.identity.iterator(); otherIdenIter.hasNext(); ) {
                prodIdentity.add(myIden.product((RelAnnotation)otherIdenIter.next()));
            }
        }
        return new ExprRelationInfo(prodRestricted, prodExcluded, prodIdentity,
                                    RelationType.product(_type, other_._type),
                                    _scopedSigsInfo);
    }

    public ExprRelationInfo transpose() {
        Mapper transposeMapper = new Mapper() {
                public Object map(Object obj_) {
                    return ((RelAnnotation)obj_).transpose();
                }};
        Set resultRestricted = Util.map(restrictedTo, transposeMapper);
        Set resultExcluded = Util.map(excluded, transposeMapper);
        Set resultIdentity = Util.map(identity, transposeMapper);
        RelationType resultType = _type.transpose();

        return new ExprRelationInfo(resultRestricted, resultExcluded,
                                    resultIdentity,
                                    resultType, _scopedSigsInfo);
    }

    private boolean _canIntersect(final ExprRelationInfo other_) {
        // (some x : this.restricted, y : other_.restricted | some x & y) &&
        // (some x : this.restricted | all y : other_.excluded | x !in y) &&
        // (some y : other_.restricted | all x : this.excluded | y !in x)
        boolean myNotRestricted = restrictedTo.isEmpty();
        boolean otherNotRestricted = other_.restrictedTo.isEmpty();
        boolean someRestricted = Util.forSome(restrictedTo, new Predicate() {
                public boolean test(Object obj_) {
                    final RelAnnotation curAnnotation = (RelAnnotation)obj_;
                    return Util.forSome(other_.restrictedTo, new Predicate() {
                            public boolean test(Object obj2_) {
                                return curAnnotation.intersects((RelAnnotation)obj2_);
                            }
                        });
                }});
        // we're also fine if either info isn't restricted to anything
        someRestricted |= myNotRestricted || otherNotRestricted;
        boolean notOtherExcluded = Util.forSome(restrictedTo, new Predicate() {
                public boolean test(Object obj_) {
                    final RelAnnotation curAnnotation = (RelAnnotation)obj_;
                    return Util.forAll(other_.excluded, new Predicate() {
                            public boolean test(Object obj2_) {
                                return !curAnnotation.in((RelAnnotation)obj2_);
                            }
                        });
                }});
        notOtherExcluded |= myNotRestricted;
        boolean notThisExcluded = Util.forSome(other_.restrictedTo, new Predicate() {
                public boolean test(Object obj_) {
                    final RelAnnotation curAnnotation = (RelAnnotation)obj_;
                    return Util.forAll(excluded, new Predicate() {
                            public boolean test(Object obj2_) {
                                return !curAnnotation.in((RelAnnotation)obj2_);
                            }
                        });
                }});
        notThisExcluded |= otherNotRestricted;
        return someRestricted && notOtherExcluded && notThisExcluded;
    }

    private ExprRelationInfo _onlyColumn(int column_) {
        Set /* of RelAnnotation */ resultRestricted = new TreeSet();
        for (Iterator restIter = restrictedTo.iterator(); restIter.hasNext(); ) {
            resultRestricted.add(((RelAnnotation)restIter.next()).fromColumn(column_));
        }
        // for excluded, only add if rest of columns are equal to type
        Set /* of RelAnnotation */ resultExcluded = new TreeSet();
        for (Iterator exclIter = excluded.iterator(); exclIter.hasNext(); ) {
            RelAnnotation curExcl = (RelAnnotation)exclIter.next();
            boolean allEqualType = true;
            for (int i = 0; i < curExcl.arity() && i != column_ && allEqualType; i++) {
                allEqualType &= _scopedSigsInfo.parentSigId(curExcl.relIdAt(i)) == null;
            }
            if (allEqualType) resultExcluded.add(curExcl.fromColumn(column_));
        }
        return new ExprRelationInfo(resultRestricted,
                                    resultExcluded,
                                    Collections.EMPTY_SET,
                                    new RelationType(_type.getBasicTypeAt(column_)),
                                    _scopedSigsInfo);
    }
    
    /**
     * add RelAnnotations x from toBeAdded_ to result_ iff
     * there is no RelAnnotation y in other_ s.t. x in y && x != y
     */
    private void _addIfLargest(Set toBeAdded_, Set other_, Set result_) {
        for (Iterator toAddIter = toBeAdded_.iterator(); toAddIter.hasNext(); ) {
            final RelAnnotation curAdd = (RelAnnotation)toAddIter.next();
            boolean canAdd = Util.forAll(other_, new Predicate() {
                    public boolean test(Object obj_) {
                        return !curAdd.in((RelAnnotation)obj_) || curAdd.equals(obj_);
                    }});
            if (canAdd) result_.add(curAdd);
        }
    }

    /**
     * add RelAnnotations x from toBeAdded_ to result_ iff
     * there is no RelAnnotation y in other_ s.t. y in x && x != y
     */
    private void _addIfSmallest(Set toBeAdded_, Set other_, Set result_) {
        for (Iterator toAddIter = toBeAdded_.iterator(); toAddIter.hasNext(); ) {
            final RelAnnotation curAdd = (RelAnnotation)toAddIter.next();
            boolean canAdd = Util.forAll(other_, new Predicate() {
                    public boolean test(Object obj_) {
                        return !((RelAnnotation)obj_).in(curAdd) || curAdd.equals(obj_);
                    }});
            if (canAdd) result_.add(curAdd);
        }
    }

    /**
     * add RelAnnotations x from toBeAdded_ to result_ iff
     * there is some RelAnnotation y in other_ s.t. x in y
     */
    private void _addIfSmallestAndCommon(Set toBeAdded_, Set other_, Set result_) {
        for (Iterator toAddIter = toBeAdded_.iterator(); toAddIter.hasNext(); ) {
            final RelAnnotation curAdd = (RelAnnotation)toAddIter.next();
            boolean canAdd = Util.forSome(other_, new Predicate() {
                    public boolean test(Object obj_) {
                        return curAdd.in((RelAnnotation)obj_);
                    }});
            if (canAdd) result_.add(curAdd);
        }
    }

    public Object clone() {
        Object ret = null;
        try {
            ret = super.clone();
        } catch (CloneNotSupportedException e) {
            Dbg.fatal("can't happen");
        }
        return ret;
    }

    public String toString() {
        StringBuffer ret = new StringBuffer();
        ret.append("restricted: ");
        ret.append(restrictedTo.toString());
        ret.append(", excluded: ");
        ret.append(excluded.toString());
        if (identity != null) {
            ret.append(", identity: ");
            ret.append(identity.toString());
        }
        return ret.toString();
    }
}
